i, j:. (i * j)   

latex

ProofTree

Definitions	t  T, , x:A. B(x), i  j , False, A, A  B, P  Q,
Lemmas	nat wf, le wf, ge wf, nat properties